The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 10 ms)
↳2 CdtProblem
↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtUsableRulesProof (⇔, 0 ms)
↳6 CdtProblem
↳7 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 194 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 45 ms)
↳10 CdtProblem
↳11 CdtKnowledgeProof (⇔, 0 ms)
↳12 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0, x3, x4, S(x)) → f3(x', 0, x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0, S(x)) → f3(x1, x2, x', 0, x)
f4(S(x'), S(x), x3, x4, 0) → 0
f4(S(x), 0, x3, x4, 0) → 0
f2(x1, x2, S(x'), S(x), 0) → 0
f2(x1, x2, S(x), 0, 0) → 0
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0, x5) → 0
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0) → 0
f5(x1, x2, x3, x4, 0) → 0
f4(0, x2, x3, x4, x5) → 0
f3(x1, x2, x3, x4, 0) → 0
f2(x1, x2, 0, x4, x5) → 0
f1(x1, x2, x3, x4, 0) → 0
f0(x1, 0, x3, x4, x5) → 0

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F4(S(z0), S(z1), z2, z3, 0) → c2
F4(S(z0), 0, z1, z2, 0) → c3
F4(0, z0, z1, z2, z3) → c4
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F2(z0, z1, S(z2), S(z3), 0) → c7
F2(z0, z1, S(z2), 0, 0) → c8
F2(z0, z1, 0, z2, z3) → c9
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F0(z0, S(z1), z2, 0, z3) → c11
F0(z0, 0, z1, z2, z3) → c12
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F6(z0, z1, z2, z3, 0) → c14
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F5(z0, z1, z2, z3, 0) → c16
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F3(z0, z1, z2, z3, 0) → c18
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
F1(z0, z1, z2, z3, 0) → c20
S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F4(S(z0), S(z1), z2, z3, 0) → c2
F4(S(z0), 0, z1, z2, 0) → c3
F4(0, z0, z1, z2, z3) → c4
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F2(z0, z1, S(z2), S(z3), 0) → c7
F2(z0, z1, S(z2), 0, 0) → c8
F2(z0, z1, 0, z2, z3) → c9
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F0(z0, S(z1), z2, 0, z3) → c11
F0(z0, 0, z1, z2, z3) → c12
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F6(z0, z1, z2, z3, 0) → c14
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F5(z0, z1, z2, z3, 0) → c16
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F3(z0, z1, z2, z3, 0) → c18
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
F1(z0, z1, z2, z3, 0) → c20
K tuples:none
Defined Rule Symbols:

f4, f2, f0, f6, f5, f3, f1

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 12 trailing nodes:

F3(z0, z1, z2, z3, 0) → c18
F0(z0, 0, z1, z2, z3) → c12
F2(z0, z1, S(z2), 0, 0) → c8
F0(z0, S(z1), z2, 0, z3) → c11
F2(z0, z1, 0, z2, z3) → c9
F2(z0, z1, S(z2), S(z3), 0) → c7
F4(S(z0), 0, z1, z2, 0) → c3
F5(z0, z1, z2, z3, 0) → c16
F1(z0, z1, z2, z3, 0) → c20
F6(z0, z1, z2, z3, 0) → c14
F4(0, z0, z1, z2, z3) → c4
F4(S(z0), S(z1), z2, z3, 0) → c2

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
K tuples:none
Defined Rule Symbols:

f4, f2, f0, f6, f5, f3, f1

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
We considered the (Usable) Rules:none
And the Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F0(x1, x2, x3, x4, x5)) = x2   
POL(F1(x1, x2, x3, x4, x5)) = x2   
POL(F2(x1, x2, x3, x4, x5)) = x1   
POL(F3(x1, x2, x3, x4, x5)) = x1   
POL(F4(x1, x2, x3, x4, x5)) = x1   
POL(F5(x1, x2, x3, x4, x5)) = x1   
POL(F6(x1, x2, x3, x4, x5)) = x2   
POL(S(x1)) = [1] + x1   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c10(x1)) = x1   
POL(c13(x1)) = x1   
POL(c15(x1)) = x1   
POL(c17(x1)) = x1   
POL(c19(x1)) = x1   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
K tuples:

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
We considered the (Usable) Rules:none
And the Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F0(x1, x2, x3, x4, x5)) = x4   
POL(F1(x1, x2, x3, x4, x5)) = [1] + x3   
POL(F2(x1, x2, x3, x4, x5)) = x3   
POL(F3(x1, x2, x3, x4, x5)) = x3 + x4   
POL(F4(x1, x2, x3, x4, x5)) = x3 + x4   
POL(F5(x1, x2, x3, x4, x5)) = x3   
POL(F6(x1, x2, x3, x4, x5)) = x3   
POL(S(x1)) = [1] + x1   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c10(x1)) = x1   
POL(c13(x1)) = x1   
POL(c15(x1)) = x1   
POL(c17(x1)) = x1   
POL(c19(x1)) = x1   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
K tuples:

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(11) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
Now S is empty

(12) BOUNDS(1, 1)